Nuprl Lemma : R-sub-plus-left
0,22
postcript
pdf
A
,
B
:Realizer.
A
A
B
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
P
&
Q
,
P
Q
Lemmas
R-sub-lemma1
,
es
realizer
wf
origin
A, B:Realizer. A 
A 
B A, B:Realizer. A A B x:A. B(x)
T
Q